プログラム意味論の基礎 命題4.1
$ P(n) = \forall \sigma \in State. Q(\sigma, n) \Rightarrow R(\sigma)
$ Q(\sigma, n) = \sigma(X) > 0 \land \sigma(Y) > 0 \land \sigma(X) + \sigma(Y) \le n
$ R(\sigma) = \exist\sigma' \in State. (EUCLID, \sigma) \longrightarrow^\star (skip, \sigma')
とすると、証明する命題は$ \forall n \in Nat. P(n)である。これを帰納法で示すには
1. $ P(0)
2. $ \forall n > 0. P(n - 1) \Rightarrow P(n)
を示せばよい。
1. どんな$ \sigma \in Stateを持ってこようと$ Q(\sigma, 0)は成り立たないので、$ n = 0のとき$ Q(\sigma, 0) \Rightarrow R(\sigma)が成り立つ。
すなわち$ P(0)である。
2.$ n > 0の場合。帰納法を使うので$ P(n - 1)を仮定することが大事。
$ \sigma \in Stateとする。
$ \sigma(X) = \sigma(Y)のとき(ここでは帰納法の仮定は使わない)。本に書いてあるように$ (EUCLID, \sigma) \longrightarrow^\star (skip, \sigma)なので、$ Q(\sigma, n)の真偽値に関係なく$ R(\sigma)である。$ Q(\sigma, n) \Rightarrow R(\sigma)が成り立つには$ Q(\sigma, n)が真のときに$ R(\sigma)も真でありさえすればよいので、$ Q(\sigma, n) \Rightarrow R(\sigma)である。
$ \sigma(X) < \sigma(Y)のとき。まず
$ Q(\sigma, n) \tag{1}
と仮定する。
帰納法の仮定より$ P(n - 1)、すなわち
$ \forall \sigma \in State. Q(\sigma, n - 1) \Rightarrow R(\sigma) \tag{2}
である。
$ \sigma_1 = \sigma\{Y \mapsto \sigma(Y) - \sigma(X)\}とする。
$ \sigma(X) = \sigma_1(X)であり、(1)より$ \sigma(X) > 0なので$ \sigma_1(X) + \sigma_1(Y) < \sigma(X) + \sigma(Y)が成り立つ。
また、(1)より$ \sigma(X) + \sigma(Y) \leq nなので$ \sigma_1(X) + \sigma_1(Y) \leq n - 1 < nが成り立つ。
これと、$ \sigma_1の定義と(1)より$ \sigma(X) = \sigma_1(X) > 0であり、$ \sigma(X) < \sigma(Y)より$ \sigma_1(Y) > 0なので$ Q(\sigma_1, n - 1)が成り立つ。
これと(2)より$ R(\sigma_1)なので、ある$ \sigma'が存在して$ (EUCLID, \sigma_1) \longrightarrow^\star (skip, \sigma')である。本に書いてあるように$ (EUCLID, \sigma) \longrightarrow^\star (EUCLID, \sigma_1)なので、$ (EUCLID, \sigma) \longrightarrow^\star (skip, \sigma')(つまり$ R(\sigma))である。
よって$ Q(\sigma, n) \Rightarrow R(\sigma)が成り立つ。
$ \sigma(X) > \sigma(Y)のときは省略。